#include "monotone_framework.hpp"

template <typename L>
MonotoneFramework<L>::MonotoneFramework(CFGvisitorFlatInfo *_g)
:	g(_g) 
{
	analysis.resize(g->labels.size());
}

template <typename L>
void MonotoneFramework<L>::run_worklist() {
	const set<label_t>& E = this->E();
	list<edge> F = this->F();

	w = F;
	for (int ell = 0; ell < this->g->labels.size(); ell++) {
		if (E.count(ell))	analysis[ell] = iota();
		else				analysis[ell] = bottom();
	}

	while (!w.empty()) {
		edge ell_ellp = w.front();
		w.pop_front(); // Mutate w: remove the head (aka front)

		label_t ell = ell_ellp.first;
		label_t ellp = ell_ellp.second; // ell prime

		/**
		 * f_ell returns the result of applying the transfer function.
		 * But we need to know which transfer function to apply, which is dependant on the statement in question.
		 * Hence we must also let f_ell know which label it is operating on.
		 */
		L new_info = this->f_ell(analysis[ell], ell);	// Try to find new (ie more) information from current information
		L curr_info = analysis[ellp];	// Current information
		if (this->square_nsubseteq(new_info, curr_info)) // Check if new_info contains more than curr_info
		{
			analysis[ellp] = this->square_cup(curr_info, new_info); // Update the current information with the newly found

#ifdef BETTER
			/*
			 * XXX: This code does not work yet
			 */
			auto ell_outgoing = this->g->labels[ellp]->outgoing_edges();
			for (auto it = ell_outgoing.begin(); it != ell_outgoing.end(); ++it) {
				label_t src = (*it)->getSource()->label();
				label_t dst = (*it)->getDestination()->label();
				if (this->is_backwards()) std::swap(src,dst);
				edge e = make_pair(src, dst);
				w.push_front(e);
			}
#else
			for (list<edge>::iterator it = F.begin(); it != F.end(); ++it) {
				edge e = *it;
				if (e.first == ellp) {
					w.push_front(e);
				}
			}
#endif
		}
	} /* while */

	this->MFP_open.resize(this->g->labels.size());
	this->MFP_fill.resize(this->g->labels.size());

	for (int ell = 0; ell < this->g->labels.size(); ell++) {
		this->MFP_open[ell] = analysis[ell];
		this->MFP_fill[ell] = f_ell(analysis[ell], ell);
	}
} /* run_worklist */


////////////////////////////////////////////////////////////////////////////////

ReachingDefs::ReachingDefs(CFGvisitorFlatInfo *_g)
: ForwardAnalysis(_g) {
	// Nothing here
}

void ReachingDefs::run() {
	this->run_worklist();
}

set<label_t> ReachingDefs::E() const {
	set<label_t> ret;
	ret.insert(this->g->init);
	return ret;
}

RD ReachingDefs::f_ell(RD analysis_ell, label_t ell) const {
	assert(analysis[ell] == analysis_ell);

	RD ret;
	RD kill;
	RD gen;

	CFGvertex *n = this->g->labels[ell];

	if (auto match = x_eq_a(n)) {
		this->compute_kill(match->x->name, kill); // kill
		gen.insert(make_pair(match->x->name, ell)); // gen
	}

	if (auto match = read_x(n)) {
		this->compute_kill(match->x->name, kill); // kill
		gen.insert(make_pair(match->x->name, ell)); // gen
	}

	if (auto match = Aa1_eq_a2(n)) { // We don't kill for array assignments
		gen.insert(make_pair(match->A->name, ell)); // only gen 
	}

	if (auto match = read_Aa1(n)) {
		gen.insert(make_pair(match->A->name, ell)); // only gen 
	}
	
	ret = set_union(set_remove(analysis_ell, kill), gen);
	return ret;
}

RD ReachingDefs::iota() const {
	RD empty;
	return empty;
}

RD ReachingDefs::bottom() const {
	RD empty;
	return empty;
}

bool ReachingDefs::square_nsubseteq(RD arg1, RD arg2) const {
	bool subseteq = includes(arg2.begin(), arg2.end(), arg1.begin(), arg1.end());
	return !subseteq;
}

RD ReachingDefs::square_cup(RD arg1, RD arg2) const {
	return ::set_union(arg1, arg2);
}

void ReachingDefs::compute_kill(string name_match, RD& kill) const {
	for (label_t nn_ell = 0; nn_ell < this->g->labels.size(); nn_ell++) {
		CFGvertex *nn = this->g->labels[nn_ell];

		ASTvisitorDefs def_vistor;
		ASTnode *visitee = NULL;

		// There can only be defs in boxes -- not diamonds
		if (TRY_TYPE(box*, nn_box, nn)) {
			visitee = nn_box->payload;
		}

		def_vistor.StartVisit(visitee);

		if (def_vistor.getDefs().count(name_match)) {
			kill.insert(make_pair(name_match, nn_ell));
		}
	}
}


///////////////////////////////////////////////////////////////////////////////

LiveVariable::LiveVariable(CFGvisitorFlatInfo *_g)
: BackwardAnalysis(_g) {
	// Nothing here
}

void LiveVariable::run() {
	this->run_worklist();
}

set<label_t> LiveVariable::E() const {
	return this->g->final;
}

LV LiveVariable::f_ell(LV analysis_ell, label_t ell) const {
	assert(analysis[ell] == analysis_ell);

	CFGvertex *n = this->g->labels[ell];
	pair<LV/*gen*/,LV/*kill*/> gen_kill = LiveVariable::compute_kill_gen(n);
	
	LV ret;
	LV gen = gen_kill.first;
	LV kill = gen_kill.second;

	ret = set_union(set_remove(analysis_ell, kill), gen);
	return ret;
}

LV LiveVariable::iota() const {
	LV empty;
	return empty;
}

LV LiveVariable::bottom() const {
	LV empty;
	return empty;
}

bool LiveVariable::square_nsubseteq(LV arg1, LV arg2) const {
	bool subseteq = ::subset(arg1, arg2);
	return !subseteq;
}

LV LiveVariable::square_cup(LV arg1, LV arg2) const {
	return ::set_union(arg1, arg2);
}

LV LiveVariable::FV(ASTnode *a) {
	LV ret;

	ASTvisitorFV afv;
	afv.StartVisit(a);

	auto afv_FV = afv.getFV();
	for (auto it = afv_FV.begin(); it != afv_FV.end(); ++it) {
		lvalue *l = *it;
		ret.insert(l->name);
	}

	return ret;
}

pair<LV/*gen*/,LV/*kill*/> LiveVariable::compute_kill_gen(CFGvertex *n) 
{
	LV kill;
	LV gen;

	if (auto match = x_eq_a(n)) {
		kill.insert(match->x->name); // Only kill the variabel.
		LV fv = LiveVariable::FV(match->a);
		gen.insert(fv.begin(), fv.end());
	}

	if (auto match = read_x(n)) {
		kill.insert(match->x->name);
		/* Don't generate anything */
	}

	if (auto match = write_a(n)) {
		/* Don't kill anything */
		LV fv = LiveVariable::FV(match->a);
		gen.insert(fv.begin(), fv.end());
	}

	if (auto match = Aa1_eq_a2(n)) {
		/* Don't kill anything */
		LV fv1 = LiveVariable::FV(match->a1);
		LV fv2 = LiveVariable::FV(match->a2);
		gen.insert(fv1.begin(), fv1.end());
		gen.insert(fv2.begin(), fv2.end());
	}

	if (auto match = read_Aa1(n)) {
		/* Don't kill anything */
		LV fv1 = LiveVariable::FV(match->a1);
		gen.insert(fv1.begin(), fv1.end());
	}
	
	if (auto match = b(n)) {
		/* Don't kill anything */
		LV fv = LiveVariable::FV(match->b);
		gen.insert(fv.begin(), fv.end());
	}
	
	return make_pair(gen, kill);
}

////////////////////////////////////////////////////////////////////////////////

DetectionSign::DetectionSign(CFGvisitorFlatInfo *_g, ASTnode *_root) 
:	ForwardAnalysis(_g), S_star(_root)
{
	// Nothing here
}
void DetectionSign::run() {
	this->run_worklist();
}

set<label_t> DetectionSign::E() const {
	set<label_t> ret;
	ret.insert(this->g->init);
	return ret;	
}
DS DetectionSign::f_ell(DS sigma, label_t ell) const {
	assert(analysis[ell] == sigma);
	
	CFGvertex *n = this->g->labels[ell];

	if (auto match = skip(n)) {
		return sigma;
	}
	
	if (auto match = x_eq_a(n)) {
		signs sign_of_a = getSign(match->a, sigma);
		sigma[match->x->name] = sign_of_a;
	}

	if (auto match = read_x(n)) {
		sigma[match->x->name] = signs({"+","-","0"});
	}

	if (auto match = Aa1_eq_a2(n)) {
		signs sign_of_a2 = getSign(match->a2, sigma);
		sigma[match->A->name] = set_union(sigma[match->A->name], sign_of_a2);
	}

	if (auto match = read_Aa1(n)) {
		sigma[match->A->name] = signs({"+","-","0"});
	}

	return sigma; // default to the identity function
}
DS DetectionSign::iota() const {
	DS ret;

	ASTvisitorFV afv;
	afv.StartVisit(this->S_star);

	auto afv_FV = afv.getFV();
	
	for_each(afv_FV, [this,&ret](lvalue *x){
		ret[x->name].insert("0");	// We say all variables are initialized to zero
	});
	
	return ret;
}
DS DetectionSign::bottom() const {
	DS empty;
	return empty;	
}
bool DetectionSign::square_nsubseteq(DS arg1, DS arg2) const {
	bool subset = true;
	
	/*
	 * for at subset==true, så skal arg2 være større end eller lige så stor som arg1
	 */
	
	for (DS::iterator it = arg1.begin(); it != arg1.end(); ++it) {
		const string& var = it->first;
		signs& sig1 = it->second;

		bool var_found = (arg2.find(var) != arg2.end());
		if (!var_found) {
			subset = false;
			break;
		}
		
		signs& sig2 = arg2[var];
		if (!::subset(sig1, sig2)) {
			subset = false;
			break;
		}
	}
	
	return !subset;
}

DS DetectionSign::square_cup(DS arg1, DS arg2) const {
	DS ret = arg1;
	
	for (DS::iterator it = arg2.begin(); it != arg2.end(); ++it) {
		const string& var = it->first;
		signs& sig2 = it->second;

		bool var_found = (arg1.find(var) != arg1.end());
		if (var_found) {
			// union af value-sæts
			ret[var].insert(sig2.begin(), sig2.end());
		} else {
			ret.insert(*it);
		}
	}
	
	return ret;
}

signs DetectionSign::getSign(ASTnode *a, DS& sigma) const {
	signs ret;
	
	ASTvisitorAs As(sigma);
	Interval ia = As.get_interval(a);
	
	const bool can_be_pos = (0 < ia.lower() || 0 < ia.upper());
	const bool can_be_neg = (ia.lower() < 0 || ia.upper() < 0);
	const bool can_be_zero= (ia.lower() <= 0 && 0 <= ia.upper()); // zero between lower and upper
	
	if (can_be_pos) {ret.insert("+");}
	if (can_be_neg) {ret.insert("-");}
	if (can_be_zero) {ret.insert("0");}

	return ret;
}

////////////////////////////////////////////////////////////////////////////////

IntervalAnalysis::IntervalAnalysis(CFGvisitorFlatInfo *_g, ASTnode *_root) 
:	ForwardAnalysis(_g), S_star(_root)
{
	// Nothing here
}
void IntervalAnalysis::run() {
	this->run_worklist();
}

set<label_t> IntervalAnalysis::E() const {
	set<label_t> ret;
	ret.insert(this->g->init);
	return ret;	
}
IV IntervalAnalysis::f_ell(IV sigma, label_t ell) const {
//	assert(analysis[ell] == sigma);
	
	CFGvertex *n = this->g->labels[ell];

	if (auto match = skip(n)) {
		return sigma;
	}
	
	if (auto match = x_eq_a(n)) {
		Interval sign_of_a = getInterval(match->a, sigma);
		if (!boost::numeric::empty(sigma[match->x->name]))	// Don't update if we know this is unreachable code
			sigma[match->x->name] = sign_of_a;
	}

	if (auto match = pred(n)) {
		ASTvisitorAi Ai(sigma);
		IV new_sigma = Ai.get_new_sigma(match->predicate);

		// Predicates acts as filters, hence we say that the new sigma = intersection(old sigma, new information)
		for_each(new_sigma, [&sigma](pair<string, Interval> p){
			sigma[p.first] = interval_intersection(sigma[p.first], p.second);
		});
	}

	if (auto match = read_x(n)) {
		sigma[match->x->name] = Interval(-iint::inf(), iint::inf());
	}

	if (auto match = Aa1_eq_a2(n)) {
		Interval sign_of_a2 = getInterval(match->a2, sigma);
		sigma[match->A->name] = interval_union(sigma[match->A->name], sign_of_a2);
	}

	if (auto match = read_Aa1(n)) {
		sigma[match->A->name] = Interval(-iint::inf(), iint::inf());
	}

	return sigma; // default to the identity function
}
IV IntervalAnalysis::iota() const {
	IV ret;

	ASTvisitorFV afv;
	afv.StartVisit(this->S_star);

	auto afv_FV = afv.getFV();
	
	for_each(afv_FV, [this,&ret](lvalue *x){
		ret[x->name] = Interval(0,0);	// We say all variables are initialized to zero
	});
	
	return ret;
}
IV IntervalAnalysis::bottom() const {
	IV empty;
	return empty;
}
bool IntervalAnalysis::square_nsubseteq(IV arg1, IV arg2) const {
	bool subset = IV_subseteq(arg1, arg2);
	return !subset;
}

IV IntervalAnalysis::square_cup(IV arg1, IV arg2) const {
	IV ret = IV_union(arg1, arg2);
	return ret;
}

Interval IntervalAnalysis::getInterval(ASTnode *a, IV& sigma) const {
	ASTvisitorAi Ai(sigma);
	Interval ret = Ai.get_interval(a);
	return ret;
}
